perm filename AIMEM2.JMC[226,JMC]2 blob
sn#080572 filedate 1974-01-07 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00003 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 \\M0BDB30\M1BASI30\M2CLAR30\M3BDR40\M4SUB\M5SUP\M6GRK25\.
C00031 00003 \F2\CREFERENCES\F0
C00032 ENDMK
C⊗;
\\M0BDB30;\M1BASI30;\M2CLAR30;\M3BDR40;\M4SUB;\M5SUP;\M6GRK25;\.
\F3\CSTANFORD ARTIFICIAL INTELLIGENCE PROJECT
\CMEMO NO. 2 JULY 1963
\CSITUATIONS, ACTIONS, AND CAUSAL LAWS
\Cby John McCarthy
\F0\CAbstract:
\←=500;\→l \←=1200;\→r
\jA formal theory concerning situations,
causality and the possibility and effects of actions is
given. The theory is intended to be used by the Advice
Taker, a computer program that is to decide what to do by
reasoning. Some simple examples are given of descriptions
of situations and deductions that certain goals can be achieved.\.
\F21. INTRODUCTION\F0
\J Although formalized theories have been devised to express the most important fields
of mathematics and some progress has been made in formalizing certain empirical
sciences, there is at present no formal theory in which one can express the kind of
means-ends analysis used in ordinary life. The closest approach to such a theory of which I am
aware is made by Freudenthal in \F1Lincos\F0 [1].
Our approach to the artificial intelligence problem requires a formal theory.
Namely, we believe that human intelligence depends essentially on the fact
that we can represent in language facts about our situation, our goals, and the
effects of the various actions we can perform. Moreover, we can draw conclusions from the facts to the effect that certain
sequences of actions are likely to achieve our goals.
In \F1Programs with Common Sense\F0 [2], I discussed the advantages of having a
computer program, to be called the Advice Taker that would reason from collections
of facts about its problem and derive statements about what it could do. The name
Advice Taker came from the hope that its behavior could be improved by giving it advice in the form of new facts rather than by
rewriting the program. The reader is referred to that paper for further information
about the Advice Taker and to Minsky's paper \F1Steps Towards
Artificial Intelligence\F0 [3] for a general introduction to the subject.
The first requirement for the Advice Taker is a formal system in which facts
about situations, goals and actions can be expressed and containing the general facts
about means and ends as axioms. A start is made in this paper on providing a system meeting
the following specifications:\.
\←=350;\→l \←=1200;\→r
1. General properties of causality and certain obvious but until
\jnow unformalized facts about the possibility and results of
actions are given as axioms.\.
2. \jIt is a logical consequence of the facts of a situation and
general axioms that certain persons can achieve certain goals
by taking certain actions.\.
3. The formal descriptions of situations should correspond as
\jclosely as possible to what people may reasonably be presumed
to know about them when deciding what to do.\.
\F22. SITUATIONS AND FLUENTS\F0
\J One of the basic entities in our theory is the situation. Intuitively,
a situation is the complete state of affairs at some instant of time. The laws
of motion of a system determine from a situation all future situations. Thus
a situation corresponds to the notion in physics of a point in phase space. In
physics, laws are expressed in the form of differential equations which give the
complete motion of the point in phase space.
Our system is not intended for the complete description of situations nor for
the description of complete laws of motion. Instead, we deal with partial descriptions of situations and partial
laws of motion. Moreover, the emphasis is on the simple qualitative laws of everyday
life rather than on the quantitative laws of physics. As an example, take the fact
that if it is raining and I go outside I will get wet.
Since a situation is a complete state of affairs, we can never describe
a situation completely, and therefore we provide no notation for doing so in our
theory. Instead, we state facts about situations in the language of an extended
predicate calculus. Examples of such facts are:\.
1. raining (s)
meaning that it is raining in situation s
2. time (s) = 1963.7205
\jgiving the value of the time in situation s. It will usually
prove convenient to regard the time as a function of the
situation rather than vice versa. The reason for this is that
the numerical value of the time is known and important only
where the laws of physics are being used.\.
3. at(I,home,s) or at(I,home)(s)
\jmeaning that I am at home in situation s. We prefer and will
use the second of the given notations that isolates the
situation variable since in most, if not all cases, we will
be able to suppress it completely.\.
\J We shall not describe in this memorandum the logical system we intend to use.
Basically, it is a predicate calculus, but we shall use the λ-notation and if necessary
conditional expressions as in LISP or ALGOL. We shall extend the meaning of the
Boolean operators to operate on predicates. Thus by\.
at(I,home) ∧ raining
we mean the same as
λs.at(I,home)(s) ∧ raining(s)
\J A predicate or function whose argument is a situation will be called a
\F1fluent\F0, the former being called a \F1propositional fluent\F0. Thus, \F1raining,
time,\F0 and \F1at(I,home)\F0 are all fluents, the first and last being propositional
fluents.
The term was used by Newton for a physical quantity that depends on time, and
according to my limited understanding of what he meant, the present use of the term
is justified.
In our formulas we will usually manage to use the fluents without explicitly
writing variables representing situations. This corresponds to the use of random
variables in probability theory without using variables representing points in the sample
space even though random variables are supposed to be regarded as functions defined
on a sample space.
In fact we shall go further and give an interpretation of our theory as a
sort of modal logic in which the fluents are not regarded as functions at all.\.
\F23. CAUSALITY\F0
\J In order to express causal laws we introduce the second order predicate cause.
The statement\.
\Ccause(π)(s)
\Jwhere π is a propositional fluent intended to mean that the situation s will lead
in the future to a situation that satisfies the fluent π. Thus, cause(π) is itself
a propositional fluent. As an example of its use we write\.
∀s.∀p.[person(p)∧raining∧outside(p)⊃cause(wet(p))](s)
\Jwhich asserts that a person who is outside when it is raining will get wet. We shall
make the convention that if π is a fluent then\.
\C∀π
means the same as
\C∀s.π(s).
\J With this convention we can write the previous statement as\.
∀∀p.person(p)∧raining∧outside(p)⊃cause(wet(p))
\Jwhich suppresses explicit mention of situations. As a second example we give a special
case of the law of falling bodies in the form:\.
∀∀t.∀b.∀t'.∀h.(real(t)∧real(t')∧real(h)∧body(b)∧unsupported(b)∧[height(b)=h]∧
[1/2gt\F52\F0<h]∧[time=t'])⊃cause(height(b)=h-1/2gt\F52\F0∧time=t'=t)
\J The concept of causality is intended to satisfy the two following general laws,
which may be taken as axioms:\.
C1. ∀. cause(π)∧[∀.π⊃\F6r\F0]⊃cause(\F6r\F0)
C2. ∀. cause (cause(π))⊃cause(π)
C3. ∀. cause(π\F41\F0)∨cause(π\F42\F0)⊃cause(π\F41\F0∨π\F42\F0)
\J The fact that we can suppress explicit mention of situations has the
following interesting consequence. Instead of regarding the π's as predicates we may regard them as
propositions and regard \F1cause\F0 as a new modal operator. The operator ∀ seems
then to be equivalent to the N (necessary) operator of ordinary modal logic.
Conversely, it would appear that modal logic of necessity might be regarded as a monadic predicate calculus where all quantifiers
are over situations.
In the present case of causality, we seem to have our choice of how to proceed.
Regarding the system as a modal logic seems to have the following two advantages.\.
1. \jIf we use the predicate calculus interpretation we require
second order predicate calculus in order to handle cause(π)(s), while if
we take the modal interpretation we can get by with first order predicate calculus.\.
2. \jWe shall want decision procedures or at least proof procedures
for as much of our system as possible. If we use the modal approach many
problems will involve only substitution of constants for variables in universal
statements and will therefore fall into a fairly readily decidable domain.\.
\J Another example of causality is given by a 2-bit binary counter that counts every second.
In our formalism its behavior may be described by the statement:\.
∀∀t ∀x\F40\F0∀x\F41\F0/ time = t∧bit∞ = x\F40\F0∧bit1 = x\F41\F0⊃cause
(time = t+1∧(bit 0 = x\F40\F0 1)∧bit 1 =x\F41\F0 (x\F40\F0∧1)))
\JIn this example \F1time, bit\F0∞, and \F1bit1\F0 are fluents while t, x\F40\F0
and x\F41\F0 are numerical variables. The distinction is made clearer if we use the more
longwinded statement\.
∀s∀t∀x\F40\F0∀x\F41\F0.time(s)=t∧bit0(s)==x\F40\F0∧bit1(s)=x\F41\F0⊃
cause(λs'.time(s')=t+1∧(bit0(s')=x\F40\F0 1)∧bit1(s')=x\F41\F0 (x\F40\F0∧)))(s)
\JIn this case, however, we can rewrite the statement in the form
∀s.cause(λs'.[time(s')=time(s)+1]∧[bit0(s')=bit0(s) 1]∧
[bit1(s')=bit1(s) (bit0(s)∧1)])(s)
Thus we see that the suppression of explicit mention of the situations forced us to introduce
the auxiliary quantities t, x\F40\F0, and x\F41\F0 which are required because
we can no longer use functions of two different situations in the same formula.
Nevertheless, the s-suppressed form may still be worthwhile since it admits the
modal interpretation.
The time as a fluent satisfies certain axioms. The fact that there is only
one situation corresponding to a given value of the time may be expressed by the axiom\.
T1. ∀∀π∀F6r\F0∀t. cause(time=t∧π)∧cause(time=t∧\F6r\F0)⊃cause(time=t∧π∧p)
Another axiom is
T2. ∀∀t.real(t)∧t>time⊃cause(time = t)
\F24. ACTIONS AND THE OPERATOR \F1CAN\F0
\J We shall regard the fact that a person performs a certain action in a situation
as a propositional fluent. Thus\.
moves (person, object, location)(s)
\Jis regarded as asserting that \F1person moves object \F0 to \F1location\F0 in
situation s.\.
∀∀p∀o∀1. moves (p,o,1)⊃cause(at(o,1))
or in the long form
∀s∀p∀o∀1. moves(p,o,1)(s)⊃cause(λs'.at(o,1)(s'))(s)
\J In order to discuss the ability of persons to achieve goals and to perform actions we introduce the operator \F1can\F0.\.
can(p,π)(s)
\Jasserts that the person p can make the situation s satisfy. We see that can(p,π)
is a propositional fluent and that like \F1cause, can\F0 may be regarded either
as a second order predicate or a modal operator. Our most common use of \F1can\F0
will be to assert that a person can perform a certain action. Thus we write\.
can(p, moves (p,o,1))(s)
\Jto assert that in situation s, the person p can move the object o to location 1.\.
The operator \F1can\F0 satisfies the axioms
K1. ∀∀π ∀\F6r\F0 ∀p. [can (p,π)∧(π⊃\F6r\F0)⊃can(p,\F6r\F0]
K2. ∀∀π ∀p\F41\F0 ∀p\F42\F0. [~can(p\F41\F0,π)∧can(p\F41\F0~π)]
K3. ∀∀p ∀π∀\F6r\F0 [can(p,π)∨can(p,\F6r\F0)⊃can(p,π∨\F6r\F0)]
Using K1 and
can(p,moves(p,o,1))
and
∀∀\F6r\F0 ∀o ∀1. moves (p,o,1)⊃cause(at(o,1))
we can deduce
can(p,cause(at(o,1)))
\Jwhich shows that the operators \F1can\F0 and \F1cause\F0 often show up in the same formula.
The ability of people to perform joint actions can be expressed by formulas like\.
can(p\F41\F0, can(p\F42\F0,marry(p\F41\F0,p\F42\F0)))
which suggests the commutative axiom
K4. ∀∀p\F41\F0 ∀p\F42\F0 ∀π.can(p\F41\F0,can(p\F42\F0,π))⊃can(p\F42\F0,can(p\F41\F0,π))
A kind of transititivity is expressed by the following:\.
\←=450;\→l \←=1150;\→r
\F1\CTheorem\F0 - From
\j1) can(p,cause(π))
and
2) ∀.π⊃can(p,cause(\F6r\F0))
it follows that
3) can(p,cause(can(p,cause(\F6r\F0))))
\F1Proof\F0 - Substitute can(p,cause(\F6r\F0)) for \F6r\F0 in axiom C1 and substitute cause(π)
for π and cause(can(p,cause(\F6r\F0))) for \F6r\F0 in axiom K1. The conclusion then follows by
propositional calculus.\.
\J In order to discuss the achievement of goals requiring several consecutive
sections we introduce \F1canult(p,π)
which is intended to mean that the person p
can ultimately bring about a situation satisfying π. We connect it with \F1can\F0
and \F1cause\F0 by means of the axiom\.
KC1. ∀.∀p∀π.π∨can(p,cause(canult(p,π)))⊃canult(p,π)
\J This axiom partially corresponds to the LISP-type recursive definition\.
canult(p,π) = π∨can(p,cause(canult(p,π)))
We also want the axiom
KC2. ∀∀p∀π. cause(canult(p,π))⊃canult(p,π)
\F25. EXAMPLES\F0
1. The Monkey can get the Bananas
\J The first example we shall consider is a situation in which a monkey is in
a room where a bunch of bananas is hanging from the ceiling too high to reach. In the
corner of the room is a box, and the solution to the monkey's problem is to move the box under
the bananas and climb unto the box from which the bananas can be reached.
We want to describe the situation in such a way that it follows from our
axioms and the description that the monkey can get the bananas. In this memorandum
we shall not discuss the heuristic problem of how monkeys do or even might solve the
problem. Specifically, we shall prove that\.
canult(monkey, has(monkey,bananas))
\JThe situation is described in a very oversimplified way by the following seven
statements:
H1. ∀∀u.place(u)⊃can(monkey,move(monkey,box,u))
H2. ∀∀u ∀v ∀p move(p,v,u)⊃cause(at(v,u))
H3. ∀ can(monkey,climbs(monkey,box))
H4. ∀ ∀u∀v∀p. at(v,u)∧climbs(p,v)⊃cause(at(v,u)∧on(p,v))
H5. ∀ place(under(bananas))
H6. ∀ at(box,under(bananas))∧on(monkey,box)⊃can(monkey,reach(monkey,bananas))
H7. ∀∀p∀x. reach(p,x)⊃cause(has(p,x))
The reasoning proceeds as follows: From 1 and 5 by substitution of under(bananas)
for u and PC (propositional calculus) we get\.
1) can(monkey,move(box,under(bananas)))
Using 1) and H2 and axiom C1, we get
2) can(monkey,cause(at(box,under(bananas))))
Similarly H3 and H4 and C1 give
3) at(box)under(bananas))⊃can(monkey,cause(at(box,under(bananas))∧on(monkey,box)))
Then H6 and H7 give
4) at(box,under(bananas))∧on(monkey,box)can(monkey,cause(has(monkey,bananas)))
Now, Theorem 1 is used to combine 2), 3), and 4) to get
5) can(monkey,cause(can(monkey,cause(can(monkey,cause(has(monkey,bananas)))))))
Using KC1 we reduce this to
canult(monkey,has(monkey,bananas))
2. An Endgame
\J A simple situation in a two person game can arise were player p\F41\F0 has
two moves, but whichever he choosed player p\F42\F0 has a move that will beat him
This situation may be described as follows:
1) can(p\F41\F0,m\F41\F0)∧can(p\F41\F0,m\F42\F0)∧(m\F41\F0∨m\F42\F0)
2) [m\F41\F0⊃cause(π\F41\F0)]∧[m\F42\F0⊃cause(π\F42\F0)]
3) ∀.π\F41\F0∨π\F42\F0⊃[can(p\F42\F0,n\F41\F0)∧can(p\F42\F0,n\F42\F0)∧(n\F41\F0∨n\F42\F0)]
4) ∀.(π\F41\F0∧n\F41\F0)∨(π\F42\F0∧n\F42\F0)⊃cause(win(p\F42\F0))
We would like to be able to draw the conclusion
3) canult(p\F42\F0,win(p\F42\F0))
We proceed as follows: From 1) and 2) we get
4) cause(π\F41\F0)∨cause(π\F42\F0)
and we use axiom C3 to get
5) cause(π\F41\F0∨π\F42\F0)
Next we weaken 3) to get
6) ∀.π\F41\F0⊃can(p\F42\F0,n\F41\F0) and
7) ∀.π\F42\F0⊃can(p\F42\F0,n\F42\F0)
and then we use K1 to get
8) ∀.π\F41\F0⊃can(p\F42\F0,π\F41\F0∧n\F41\F0) and
9) ∀.π\F42\F0⊃can(p\F42\F0,π\F42\F0∧n\F42\F0)
The propositional calculus gives
10) ∀.π\F41\F0∨π\F42\F0⊃can(p\F42\F0,π\F41\F0∧n\F41\F0)∨can(p\F42\F0,π\F42\F0∧n\F42\F0)
and using K3 we get
11) ∀.π\F41\F0∨π\F42\F0⊃can(p\F42\F0,(π\F41\F0∧n\F41\F0)∨(π\F42\F0∧n\F42\F0))
which together with 4) and K1 gives
12) ∀.π\F41\F0∨π\F42\F0⊃can(p\F42\F0,cause(win(p\F42\F0)))
which together with 5) and C1 gives
13) cause(can(p\F42\F0,cause(win(p\F42\F0))))
Using the axioms for \F1canult\F0 we now get
14) canult(p\F42\F0,win(p\F42\F0)).\.
\F26. NOTE\F0
\J After finishing the bulk of this memorandum I came across \F1The Syntax
of Time Distinctions\F0 [4] by A. N. Prior. Prior defines modal operators P and F
where
P(π) means `it has been the case that π' and
F(π) means `it will be the case that π'
He subjects these operators to a number of axioms and rules of inference in
close analogy to the well-known [5] modal logic of possibility. He also interprets
this logic in a restricted predicate calculus where the variables range over times.
He then extends his logic to include a somewhat undetermined future and claims
(unconvincingly) that this logic cannot be interpreted in predicate calculus.
I have not yet made a detailed comparison of our logic with Prior's, but
here are some tentative conclusions.\.
1.\jThe causality logic should be extended to allow inference
about the past.\.
2.\jCausality logic should be extended to allow inference that
certain propositional fluents will always hold.\.
3.\jcause(π) satisfies the axioms for his F(π) which means that
his futurity theory possesses, from his point of view, non-standard
models. Namely, a collection of functions p\F41\F0(t),p\F42\F0(t)
may satisfy his futurity axioms and assign truth to p(1)∧~(Fp)(o).
In our system whis is okay because something can happen without
being caused to happen.\.
4.\jIf we combine his past an futurity axioms, our system will no
longer fit his axioms and
PF1. p⊃~F(~P(p))
PF2. p⊃~P(~F(p))
since we do not wish to say that whatever is, was always inevitable.\.
\F2\CREFERENCES\F0
1. Freudenthal, H.A., \F1LINCOS, Design of a Language for Cosmic Intercourse,
Part I\F0, Amsterdam (1960).
2. McCarthy, John, \F1Programs with Common Sense,\F2 Proceedings Symposium on
Mechanization of Thought Processes\F0, Her Majesty's Stationery
Office, London (1959).
3. Minsky, M.L., \F1Steps Toward Artificial Intelligence,\F2 Proceedings of the
IRE\F0, Vol. 29, No. 1, (January, 1961).
4. Prior, A.N., \F1The Syntax of Time Distinctions,\F2 Franciscan Studies\F0 (1958).
5. von Wright, G.H., \F1An Essay in Modal Logic\F0, Amsterdam (1951).